| Definitions |  x:A. B(x), @i: k affects only L,  , P   Q, D realizes2 es.P(es), t  T,   x. t(x), e@i. P(e), kind(e), P & Q,  A, vartype(i;x), (timed)state after e, es_state_when(es;e), ES(the_w), t.1, t.2, time(e), es_info(es), es-T(es), es-pred?(es), es_init(es), es-Trans(es), es_val(es), es_time(es), vartype(i;x),  b, P  Q, if b then t else f fi , deq-member(eq;x;L), {T}, E, loc(e), loc(e), SQType(T), (x after e), (x when e), tt, reduce(f;k;as), ff, Y, P  Q, P Q, True, r - s, r + s,  T, @i: k affects only members of L, x(s), PossibleWorld(D;w), A c B, M.ds(x), M(i), M.init(x,v), M.pre(a,s), M.ef(k,x,s,v,w), M.send(k;l;s;v;ms;i), M.frame(k affects x), M.sframe(k sends <l,tg>), M.aframe(k affects x), M.bframe(k sends on l), f(x)?z, k affects only members of L, z != f(x) P(a;z), x dom(f), mk-ma, x : v, f(x), act(e), kind(e), False, Dec(P), state_after(e), state_when(e), state_after(e), state_when(e), s.x, a = b, S  T |